1. Field of the Invention
The invention is related to the field of program analysis, and in particular, to using control flow information for performing a symbolic depth-first search of a system to perform reachability analysis and verification of the system.
2. Statement of the Problem
The design of integrated circuit devices conventionally uses hardware description languages (HDLs) to describe circuits (herein also called “systems”) at various levels of abstraction. As a circuit design evolves, designers and verification engineers conduct analysis of the circuit or device being designed to evaluate the quality of the design and to find and eliminate any inadequacies potentially leading to future problems such as impossibility or inaccuracy in performance of the system.
Invariant checking is a popular form of verifying the operation of a system, as well as for verifying the operation of software applications or program code. As used herein, system refers to software applications or program code, as well as any type of circuit expressed in a HDL or any other type of programmatic representation of the circuit. In invariant checking, a propositional formula expresses a property that should hold in all reachable states of the system. For example, an arbitration protocol should satisfy the mutual exclusion property, which states that two requesters should not be granted simultaneous access to a shared resource. If two requesters are able to simultaneously access the same resource, then the invariant fails, and the system does not function properly.
Systems modeled as Finite State Machines (FSMs) may exploit symbolic computations based on Binary Decision Diagrams (BDDs). A BDD is a data structure that represents a Boolean function. Several approaches are in use for the formal verification of invariants. Model checking is one such approach, because model checking is largely automated and produces counterexamples if the invariant does not hold. One approach to model checking is based on the computation of fixed points and typically uses BDDs for the representation of sets of states. The other approach is based on the search for a path to a state violating the property.
Using BDDs, states may be represented implicitly and explicitly. The typical BDD-based invariant-checking algorithm performs a breadth-first search (BFS) of the state space from the initial states. All states at distance k from the initial states are acquired by the k-th image computation, without explicit enumeration of either states or transitions. Whenever the BDDs that symbolically represent states and transition relations remain compact, BFS is very efficient. However, a constraint that is imposed on the order in which states are visited (i.e., distance from the initial states) often leads to sets whose representation is not compact. In addition, the requirement to compute all the states at a certain distance at once often leads to very large BDDs at the intermediate steps of some image computations.
If the set of states cannot be represented compactly, then the BFS approach runs into a state explosion problem or time limit to provide an answer to the property in question. The state explosion problem occurs when an input to the design, intended to permit analysis of the response of the system to a particular input, generates such a large number of possible output or intermediate states as to overrun any memory used in supporting the analysis. In order for model checkers to be used to find bugs and errors in software systems, the model checkers must find ways around the state explosion problem. Thus, improved solutions are needed for automated model checking of systems.